theory Design_Sec_OpenSession
imports "../Design_Instantiation"
begin
section "auxiliary lemma"
lemma Driver_Read_not_change_old:
"∀s. (⇑(Driver_Read s smc_ex_init_read zx_mgr)) = ⇑s"
using Driver_Read_def by simp
lemma Driver_Write_smc_not_change_old:
"∀s.
(⇑(fst(Driver_Write_smc s zx_mgr ZX_OKr smc_ex_init))) = (⇑s)"
using Driver_Write_smc_def by auto
lemma abs_rev_lemma:"(⇑(s⇓t)) =t" by auto
lemma TEEC_InitializeContextR_notchnew:
assumes p1: "s'=(fst (TEEC_InitializeContextR sc s name ctx1))"
shows "(s ∼. d .∼Δ s')"
using TEEC_InitializeContextR_def abstract_state_def abstract_state_rev_def vpeq_ipc_def
by (smt (verit) Pair_inject State.ext_inject State.update_convs(1)
State.update_convs(2) State.update_convs(3) State.update_convs(4) State.update_convs(5)
State.update_convs(6) StateR.ext_inject StateR.surjective p1 surjective_pairing )
lemma TEEC_FinalizeContextR_notchnew:
assumes p1: "s'=(TEEC_FinalizeContextR sc s ctx1)"
shows "(s ∼. d .∼Δ s')"
using TEEC_FinalizeContextR_def abstract_state_def abstract_state_rev_def vpeq_ipc_def
by (smt (verit) Pair_inject State.ext_inject State.update_convs(1)
State.update_convs(2) State.update_convs(3) State.update_convs(4) State.update_convs(5)
State.update_convs(6) StateR.ext_inject StateR.surjective p1 surjective_pairing )
lemma TEEC_OpenSession1R_notchnew:
assumes p1: "s'=(fst(TEEC_OpenSession1R sysconf s tct tst uuid cm cd opt mem_t))"
shows "(s ∼. d .∼Δ s')"
using TEEC_OpenSession1R_def abstract_state_def abstract_state_rev_def vpeq_ipc_def
by (smt (verit) Pair_inject State.ext_inject State.update_convs(1)
State.update_convs(2) State.update_convs(3) State.update_convs(4) State.update_convs(5)
State.update_convs(6) StateR.ext_inject StateR.surjective p1 surjective_pairing )
lemma TEE_OpenTASession1R_notchnew:
assumes p1: "s'=(fst(TEE_OpenTASession1R sysconf s))"
shows "(s ∼. d .∼Δ s')"
using TEE_OpenTASession1R_def abstract_state_def abstract_state_rev_def vpeq_ipc_def
by (smt (verit) Pair_inject State.ext_inject State.update_convs(1)
State.update_convs(2) State.update_convs(3) State.update_convs(4) State.update_convs(5)
State.update_convs(6) StateR.ext_inject StateR.surjective p1 surjective_pairing )
lemma TEE_OpenTASession2R_notchnew:
assumes p1: "s'=(fst(TEE_OpenTASession2R sysconf s))"
shows "(s ∼. d .∼Δ s')"
using TEE_OpenTASession2R_def abstract_state_def abstract_state_rev_def vpeq_ipc_def
by (smt (verit) Pair_inject State.ext_inject State.update_convs(1)
State.update_convs(2) State.update_convs(3) State.update_convs(4) State.update_convs(5)
State.update_convs(6) StateR.ext_inject StateR.surjective p1 surjective_pairing )
lemma TEE_OpenTASession4R_notchnew:
assumes p1: "s'=(fst(TEE_OpenTASession4R sysconf s))"
shows "(s ∼. d .∼Δ s')"
using TEE_OpenTASession4R_def abstract_state_def abstract_state_rev_def vpeq_ipc_def
by (smt (verit) Pair_inject State.ext_inject State.update_convs(1)
State.update_convs(2) State.update_convs(3) State.update_convs(4) State.update_convs(5)
State.update_convs(6) StateR.ext_inject StateR.surjective p1 surjective_pairing )
lemma ioctrlR_notchnew:
assumes p1: "s'=(fst (ioctrlR sc s uuid opt cli ctx1 mem_t0))"
shows "(s ∼. d .∼Δ s')"
using ioctrlR_def abstract_state_def abstract_state_rev_def vpeq_ipc_def
by (smt (verit) Pair_inject State.ext_inject State.update_convs(1)
State.update_convs(2) State.update_convs(3) State.update_convs(4) State.update_convs(5)
State.update_convs(6) StateR.ext_inject StateR.surjective p1 surjective_pairing )
section "refinement proof"
subsection "TEEC side"
lemma TEEC_InitializeContextR_refine:
"∀s. fst (TEEC_InitializeContext sc (⇑s) name ctx1) = ⇑(fst (TEEC_InitializeContextR sc s name ctx1))"
using TEEC_InitializeContext_def by auto
lemma TEEC_FinalizeContextR_refine:
"∀s. (TEEC_FinalizeContext sc (⇑s) ctx1) = ⇑(TEEC_FinalizeContextR sc s ctx1)"
using TEEC_FinalizeContext_def by auto
lemma TEEC_OpenSession1R_refine:
"∀s. fst (TEEC_OpenSession1 sc (⇑s) ctx1 ses1 id1 md str opt mem_t) = ⇑(fst (TEEC_OpenSession1R sc s ctx1 ses1 id1 md str opt mem_t))"
using TEEC_OpenSession1_def TEEC_OpenSession1R_def abstract_state_def abstract_state_rev_def
by (smt (z3) State.select_convs(1) State.select_convs(2) State.select_convs(3)
State.select_convs(4) State.select_convs(5) State.select_convs(6) State.surjective
State.update_convs(1) State.update_convs(2) State.update_convs(3) State.update_convs(4)
State.update_convs(5) State.update_convs(6) fstI old.unit.exhaust)
lemma TEEC_OpenSession2R_refine:
"∀s. fst (TEEC_OpenSession2 sc (⇑s)) = ⇑(fst(TEEC_OpenSession2R sc s))"
proof -
{
fix s
let ?s'="fst(TEEC_OpenSession2R sc s)"
let ?t = "⇑s"
let ?t' = "fst(TEEC_OpenSession2 sc ?t)"
have a0:"current s=current ?t∧TEE_state s =TEE_state ?t∧exec_prime s=exec_prime ?t"
by simp
have a01:"?t' =⇑(?s')"
proof -
{
show ?thesis
proof(cases"(exec_prime s) =[]∨snd (hd (exec_prime s)) ≠TEEC_OP2∨current s≠TEE sc")
case True
then have a1:"(exec_prime s) =[]∨snd (hd (exec_prime s)) ≠TEEC_OP2∨current s≠TEE sc" by simp
have a2:"?t=?t'" using TEEC_OpenSession2_def a1 by fastforce
have a3:"s=?s'" using TEEC_OpenSession2R_def a1 by auto
show ?thesis using a2 a3 by simp
next
case False
then have a4:"¬((exec_prime s) =[]∨snd (hd (exec_prime s)) ≠TEEC_OP2∨current s≠TEE sc)" by simp
show ?thesis
proof -
{
let ?exec = "exec_prime s"
let ?p = "fst (hd (?exec))"
let ?opt = "the(param3 ?p)"
let ?uuid = "the (param1 ?p)"
let ?cli = "the (param4 ?p)"
let ?ctx1 = "the (param5 ?p)"
let ?memt0 = "(the (param10 ?p),the (param11 ?p))"
let ?s1 = "s⦇exec_prime:=tl ?exec⦈"
let ?t1 = "?t⦇exec_prime:=tl ?exec⦈"
let ?s2 = "Driver_Read ?s1 smc_ex_init_read zx_mgr"
let ?s3 = "fst(ioctrlR sc ?s2 ?uuid ?opt ?cli ?ctx1 ?memt0)"
let ?t3 = "fst(ioctrl sc ?t1 ?uuid ?opt ?cli ?ctx1 ?memt0)"
have a5:"?t1=⇑(?s1)" by auto
have a6:"?t1=⇑(?s2)" using Driver_Read_not_change_old by simp
have a71:"(?s2⇓?t3)=(?s3)" using ioctrlR_def a6
by (metis (no_types, lifting) prod.collapse prod.inject)
have a72:"?t3=⇑(?s3)" using a71 abs_rev_lemma by metis
have a8:"?s'=?s3" using a4 TEEC_OpenSession2R_def by metis
have a9:"?t'=?t3" using a4 TEEC_OpenSession2_def a0 by metis
show ?thesis using a72 a8 a9 by argo
}
qed
qed
} qed
}
then show ?thesis by blast
qed
lemma TEEC_OpenSession3R_refine:
"∀s. fst (TEEC_OpenSession3 sc (⇑s) sid) = ⇑(fst(TEEC_OpenSession3R sc s sid))"
proof -
{
fix s
let ?s'="fst(TEEC_OpenSession3R sc s sid)"
let ?t = "⇑s"
let ?t' = "fst(TEEC_OpenSession3 sc ?t sid)"
let ?exec = "exec_prime s"
let ?p = "fst (hd (?exec))"
let ?ses_id = "the (param2 ?p)"
let ?opt = "the(param3 ?p)"
let ?uuid = "the (param1 ?p)"
let ?ctx1 = "the (param5 ?p)"
let ?s1 = "s⦇exec_prime:=tl ?exec⦈"
let ?t1 = "?t⦇exec_prime:=tl ?exec⦈"
let ?s2 = "?s1⇓(initTAProcess (⇑?s1) ?opt ?uuid ?ses_id)"
let ?t2 = "initTAProcess ?t1 ?opt ?uuid ?ses_id"
let ?s3 = "TA_OpenSessionEntryPointR sc ?s2 ?opt ?uuid"
let ?t3 = "TA_OpenSessionEntryPoint sc ?t2 ?opt ?uuid"
let ?param="⦇param1=Some ?uuid,param2=Some ?ses_id,param3=None,param4=None,
param5=None,param6=None,param7=None,param8=None,param9=None,param10=None,
param11=None,param12=Some TEEC_SUCCESS, param13=None⦈"
let ?s4= "?s3⦇current:=TEE sc,exec_prime:=(?param,TEEC_OP4)#(exec_prime ?s3)⦈"
let ?t4= "?t3⦇current:=TEE sc,exec_prime:=(?param,TEEC_OP4)#(exec_prime ?t3)⦈"
have a0:"current s=current ?t∧TEE_state s =TEE_state ?t∧exec_prime s=exec_prime ?t"
by simp
have a01:"?t' =⇑(?s')"
proof(cases "?exec = []∨snd (hd ?exec)≠TEEC_OP3∨sid≠?ses_id
∨TEE sc=current s∨REE sc=current s∨current s≠?uuid")
case True
have a2:"?t=?t'" using TEEC_OpenSession3_def True by auto
have a3:"?s'=s" using TEEC_OpenSession3R_def True by auto
then show ?thesis using a2 a3 by simp
next
case False
then have a4:"¬(?exec = []∨snd (hd ?exec)≠TEEC_OP3∨sid≠?ses_id
∨TEE sc=current s∨REE sc=current s∨current s≠?uuid)" by simp
have a5:"?t1=⇑?s1" by simp
have a6:"?t2=⇑?s2" by simp
have a7:"?t3=⇑?s3" using TA_OpenSessionEntryPoint_def
TA_OpenSessionEntryPointR_def a6 by simp
have a8:"?t4=⇑?s4" using a7 by auto
have a9:"?t4=?t'" using a4 a0 TEEC_OpenSession3_def State.fold_congs(6) fst_conv
by (smt (verit) State.unfold_congs(1))
have a10:"?s4=?s'" using a4 TEEC_OpenSession3R_def State.fold_congs(6) fst_conv
TEEC_OpenSession3_def abstract_state_def abstract_state_rev_def
by (smt (verit) State.unfold_congs(1))
show ?thesis using a8 a9 a10 by argo
qed
}
then show ?thesis by blast
qed
lemma TEEC_OpenSession4R_refine:
"∀s. fst (TEEC_OpenSession4 sc (⇑s)) = ⇑(fst(TEEC_OpenSession4R sc s))"
proof -
{
fix s
let ?s'="fst(TEEC_OpenSession4R sc s)"
let ?t = "⇑s"
let ?t' = "fst(TEEC_OpenSession4 sc ?t)"
have a0:"current s=current ?t∧TEE_state s =TEE_state ?t∧exec_prime s=exec_prime ?t"
by simp
have a01:"?t' =⇑(?s')"
proof -
{
show ?thesis
proof(cases"(exec_prime s) =[]∨snd (hd (exec_prime s)) ≠TEEC_OP4∨current s≠TEE sc")
case True
then have a1:"(exec_prime s) =[]∨snd (hd (exec_prime s)) ≠TEEC_OP4∨current s≠TEE sc" by simp
have a2:"?t=?t'" using TEEC_OpenSession4_def using a1 by auto
have a3:"s=?s'" using TEEC_OpenSession4R_def using a1 by auto
show ?thesis using a2 a3 by simp
next
case False
then have a4:"¬((exec_prime s) =[]∨snd (hd (exec_prime s)) ≠TEEC_OP4∨current s≠TEE sc)" by simp
let ?exec="exec_prime s"
let ?p = "fst (hd ?exec)"
let ?tid1 =" the (param1 ?p)"
let ?ses_id =" the (param2 ?p)"
let ?res3= "the (param12 ?p)"
let ?param="⦇param1=Some ?ses_id,param2=Some ?tid1,param3=None,param4=Some ⦇login=DTC_IDENTITY,id=Some 0⦈,
param5=None,param6=None,param7=None,param8=None,param9=None,
param10=None,param11=None,param12=None,param13=None⦈"
let ?smc_ex = "⦇a0=0,a1=0,a2=0,a3= ?ses_id,a4=0,a5=0,a6=0,a7=0,u2k=0,k2u=0⦈"
let ?s1="s⦇exec_prime:=tl ?exec⦈"
let ?t1="?t⦇exec_prime:=tl ?exec⦈"
let ?s2="?s1⇓(MgrPostOperation (⇑?s1) ?tid1)"
let ?t2="MgrPostOperation ?t1 ?tid1"
let ?s3="?s2⦇current:=TEE sc,exec_prime:=(?param,TEEC_CS2)#(exec_prime ?s2)⦈"
let ?t3="?t2⦇current:=TEE sc,exec_prime:=(?param,TEEC_CS2)#(exec_prime ?t2)⦈"
let ?s4="fst(Driver_Write_smc ?s3 zx_mgr ZX_ERR_INTERNALr smc_ex_init)"
let ?s42="fst(Driver_Write_smc ?s2 zx_mgr ZX_OKr ?smc_ex)"
have a5:"?t1=(⇑?s1)" by simp
have a6:"?t2=(⇑?s2)" by simp
have a7:"?t3=(⇑?s3)" by simp
have a8:"(⇑?s3)=(⇑?s4)"
using Driver_Write_smc_not_change_old Driver_Write_smc_def by simp
have a9:"(⇑?s2)=(⇑?s42)"
using Driver_Write_smc_not_change_old Driver_Write_smc_def by simp
have a10:"?t3=(⇑?s4)" using a8 by auto
have a11:"?t2=(⇑?s42)" using a9 by auto
show ?thesis
proof(cases"?res3=TEEC_SUCCESS")
case True
then have b1:"?res3=TEEC_SUCCESS" by simp
show ?thesis
proof -
{
have b2:"?t'=?t2"
using a4 b1 a0 TEEC_OpenSession4_def
by (smt (verit, best) State.fold_congs(6) fst_conv)
have b3:"?s'=?s42"
using a4 b1 State.fold_congs(6) fst_conv
unfolding TEEC_OpenSession4R_def TEEC_OpenSession4_def
abstract_state_def abstract_state_rev_def Driver_Write_smc_def
by (smt (verit, best) State.fold_congs(6) fst_conv)
show ?thesis using b2 b3 a11 by argo
}qed
next
case False
then have b4:"?res3≠TEEC_SUCCESS" by simp
show ?thesis
proof -
{
have b5:"?t'=?t3"
using a4 b4 a0 TEEC_OpenSession4_def
by (smt (verit, best) State.unfold_congs(1) State.unfold_congs(6) fst_conv)
have b6:"?s'=?s4"
using a4 b4 unfolding TEEC_OpenSession4R_def TEEC_OpenSession4_def
abstract_state_def abstract_state_rev_def Driver_Write_smc_def
by (smt (verit, best) State.fold_congs(6) fst_conv)
show ?thesis using b5 b6 a10 by argo
}qed
qed
qed
}
qed
}
then show ?thesis by blast
qed
subsection "TEE side"
lemma TEE_OpenTASession1R_refine:
"∀s. fst (TEE_OpenTASession1 sc (⇑s)) = ⇑(fst (TEE_OpenTASession1R sc s))"
using TEE_OpenTASession1_def TEE_OpenTASession1R_def abstract_state_def abstract_state_rev_def
by (smt (z3) State.select_convs(1) State.select_convs(2) State.select_convs(3)
State.select_convs(4) State.select_convs(5) State.select_convs(6) State.surjective
State.update_convs(1) State.update_convs(2) State.update_convs(3) State.update_convs(4)
State.update_convs(5) State.update_convs(6) fstI old.unit.exhaust)
lemma TEE_OpenTASession2R_refine:
"∀s. fst (TEE_OpenTASession2 sc (⇑s)) = ⇑(fst (TEE_OpenTASession2R sc s))"
using TEE_OpenTASession2_def TEE_OpenTASession2R_def abstract_state_def abstract_state_rev_def
by (metis abs_rev_lemma fstI)
lemma TEE_OpenTASession3R_refine:
"∀s. fst (TEE_OpenTASession3 sc (⇑s) sid) = ⇑(fst(TEE_OpenTASession3R sc s sid))"
proof -
{
fix s
let ?s'="fst(TEE_OpenTASession3R sc s sid)"
let ?t = "⇑s"
let ?t' = "fst(TEE_OpenTASession3 sc ?t sid)"
let ?exec = "exec_prime s"
let ?p = "fst (hd (?exec))"
let ?ses_id = "the (param2 ?p)"
let ?opt = "the(param3 ?p)"
let ?uuid = "the (param1 ?p)"
let ?ctx1 = "the (param5 ?p)"
let ?s1 = "s⦇exec_prime:=tl ?exec⦈"
let ?t1 = "?t⦇exec_prime:=tl ?exec⦈"
let ?s2 = "?s1⇓(initTAProcess (⇑?s1) ?opt ?uuid ?ses_id)"
let ?t2 = "initTAProcess ?t1 ?opt ?uuid ?ses_id"
let ?s3 = "TA_OpenSessionEntryPointR sc ?s2 ?opt ?uuid"
let ?t3 = "TA_OpenSessionEntryPoint sc ?t2 ?opt ?uuid"
let ?param="⦇param1=Some ?uuid,param2=Some ?ses_id,param3=None,param4=None,
param5=None,param6=None,param7=None,param8=None,param9=None,param10=None,
param11=None,param12=None, param13=Some TEE_SUCCESS⦈"
let ?s4= "?s3⦇current:=TEE sc,exec_prime:=(?param,TEE_OP4)#(exec_prime ?s3)⦈"
let ?t4= "?t3⦇current:=TEE sc,exec_prime:=(?param,TEE_OP4)#(exec_prime ?t3)⦈"
have a0:"current s=current ?t∧TEE_state s =TEE_state ?t∧exec_prime s=exec_prime ?t"
by simp
have a01:"?t' =⇑(?s')"
proof(cases "?exec = []∨snd (hd ?exec)≠TEE_OP3∨sid≠?ses_id
∨TEE sc=current s∨REE sc=current s∨current s≠?uuid")
case True
have a2:"?t=?t'" using TEE_OpenTASession3_def True by auto
have a3:"?s'=s" using TEE_OpenTASession3R_def True by auto
then show ?thesis using a2 a3 by simp
next
case False
then have a4:"¬(?exec = []∨snd (hd ?exec)≠TEE_OP3∨sid≠?ses_id
∨TEE sc=current s∨REE sc=current s∨current s≠?uuid)" by simp
have a5:"?t1=⇑?s1" by simp
have a6:"?t2=⇑?s2" by simp
have a7:"?t3=⇑?s3" using TA_OpenSessionEntryPoint_def
TA_OpenSessionEntryPointR_def a6 by simp
have a8:"?t4=⇑?s4" using a7 by auto
have a9:"?t4=?t'" using a4 a0 TEE_OpenTASession3_def State.fold_congs(6) fst_conv
by (smt (verit) State.unfold_congs(1))
have a10:"?s4=?s'" using a4 TEE_OpenTASession3R_def State.fold_congs(6) fst_conv
TEE_OpenTASession3_def abstract_state_def abstract_state_rev_def
by (smt (verit) State.unfold_congs(1))
show ?thesis using a8 a9 a10 by argo
qed
}
then show ?thesis by blast
qed
lemma TEE_OpenTASession4R_refine:
"∀s. fst (TEE_OpenTASession4 sc (⇑s)) = ⇑(fst (TEE_OpenTASession4R sc s))"
using TEE_OpenTASession4_def TEE_OpenTASession4R_def abstract_state_def abstract_state_rev_def
by (metis abs_rev_lemma fstI)
section "security proof"
subsection "TEEC side"
subsubsection "TEEC_InitializeContextR"
lemma TEEC_InitializeContextR_integrity:
assumes p1: "a = hyperc' (TEEC_INITIALIZECONTEXT tn tctext)"
shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_eventR s a)) ∖↝ d)
∧ (s, s') ∈ exec_eventR a ⟶ (s ∼. d .∼Δ s')"
proof -
{
fix s' s d
assume a1: "reachable0 s"
assume a2: "((the (domain_of_eventR s a)) ∖↝ d)"
assume a3: "(s,s') ∈ exec_eventR a"
have b1:"s'=fst (TEEC_InitializeContextR sysconf s tn tctext)"
using exec_eventR_def a3 p1 by simp
have b2:"(s ∼. d .∼Δ s')" using TEEC_InitializeContextR_notchnew b1 by blast
} then show ?thesis by blast
qed
lemma TEEC_InitializeContextR_integrity_e:
"integrity_new_e (hyperc' (TEEC_INITIALIZECONTEXT tn tctext))"
using TEEC_InitializeContextR_integrity integrity_new_e_def
by metis
lemma TEEC_InitializeContextR_weak_confidentiality:
assumes p1: "a = hyperc' (TEEC_INITIALIZECONTEXT tn tctext)"
shows "∀ d s t.
reachable0 s ∧
reachable0 t ∧
(s ∼. d .∼ t) ∧
((domain_of_eventR s a) = (domain_of_eventR t a)) ∧
(get_exec_primeR s=get_exec_primeR t) ∧
((the (domain_of_eventR s a)) ↝ d) ∧
(s ∼. (the (domain_of_eventR s a)) .∼ t) ⟶
(∀ s' t'. (s, s') ∈ exec_eventR a ∧ (t, t') ∈ exec_eventR a ⟶ (s' ∼. d .∼Δ t'))"
proof -
{
fix s t d s' t'
assume a1:"reachable0 s"
assume a2:"reachable0 t"
assume a3:"s∼.d.∼t"
assume a31:"exec_prime s=exec_prime t"
assume a4:"(domain_of_eventR s a) = (domain_of_eventR t a)"
assume a5:"(the (domain_of_eventR s a)) ↝ d"
assume a6:"s ∼. (the (domain_of_eventR s a)) .∼ t"
assume a7:"(s, s') ∈ exec_eventR a"
assume a8:"(t, t') ∈ exec_eventR a"
have b1:"s'=fst (TEEC_InitializeContextR sysconf s tn tctext)"
using exec_eventR_def a7 p1 by simp
have b2:"t'=fst (TEEC_InitializeContextR sysconf t tn tctext)"
using exec_eventR_def a8 p1 by simp
have b3:"s' ∼. d .∼Δ t'" using b1 b2 TEEC_InitializeContextR_notchnew a3 vpeqR_def
by (meson vpeq_ipc_symmetric_lemma vpeq_ipc_transitive_lemma)
} then show ?thesis using get_exec_primeR_def
by (smt (verit, best) prod.inject)
qed
lemma TEEC_InitializeContextR_weak_confidentiality_e:
"weak_confidentiality_new_e (hyperc' (TEEC_INITIALIZECONTEXT tn tctext))"
using TEEC_InitializeContextR_weak_confidentiality weak_confidentiality_new_e_def get_exec_primeR_def
by (smt (verit) Pair_inject)
subsubsection "TEEC_FinalizeContextR"
lemma TEEC_FinalizeContextR_integrity:
assumes p1: "a = hyperc' (TEEC_FINALIZECONTEXT tctext)"
shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_eventR s a)) ∖↝ d)
∧ (s, s') ∈ exec_eventR a ⟶ (s ∼. d .∼Δ s')"
proof -
{
fix s' s d
assume a1: "reachable0 s"
assume a2: "((the (domain_of_eventR s a)) ∖↝ d)"
assume a3: "(s,s') ∈ exec_eventR a"
have b1:"s'=(TEEC_FinalizeContextR sysconf s tctext)"
using exec_eventR_def a3 p1 by simp
have b2:"(s ∼. d .∼Δ s')" using TEEC_FinalizeContextR_notchnew b1 by blast
} then show ?thesis by blast
qed
lemma TEEC_FinalizeContextR_integrity_e:
"integrity_new_e (hyperc' (TEEC_FINALIZECONTEXT tctext))"
using TEEC_FinalizeContextR_integrity integrity_new_e_def
by metis
lemma TEEC_FinalizeContextR_weak_confidentiality:
assumes p1: "a = hyperc' (TEEC_FINALIZECONTEXT tctext)"
shows "∀ d s t.
reachable0 s ∧
reachable0 t ∧
(s ∼. d .∼ t) ∧
((domain_of_eventR s a) = (domain_of_eventR t a)) ∧
(get_exec_primeR s=get_exec_primeR t) ∧
((the (domain_of_eventR s a)) ↝ d) ∧
(s ∼. (the (domain_of_eventR s a)) .∼ t) ⟶
(∀ s' t'. (s, s') ∈ exec_eventR a ∧ (t, t') ∈ exec_eventR a ⟶ (s' ∼. d .∼Δ t'))"
proof -
{
fix s t d s' t'
assume a1:"reachable0 s"
assume a2:"reachable0 t"
assume a3:"s∼.d.∼t"
assume a31:"exec_prime s=exec_prime t"
assume a4:"(domain_of_eventR s a) = (domain_of_eventR t a)"
assume a5:"(the (domain_of_eventR s a)) ↝ d"
assume a6:"s ∼. (the (domain_of_eventR s a)) .∼ t"
assume a7:"(s, s') ∈ exec_eventR a"
assume a8:"(t, t') ∈ exec_eventR a"
have b1:"s'=(TEEC_FinalizeContextR sysconf s tctext)"
using exec_eventR_def a7 p1 by simp
have b2:"t'=(TEEC_FinalizeContextR sysconf t tctext)"
using exec_eventR_def a8 p1 by simp
have b3:"s' ∼. d .∼Δ t'" using b1 b2 TEEC_FinalizeContextR_notchnew a3 vpeqR_def
by (meson vpeq_ipc_symmetric_lemma vpeq_ipc_transitive_lemma)
} then show ?thesis using get_exec_primeR_def
by (smt (verit, best) prod.inject)
qed
lemma TEEC_FinalizeContextR_weak_confidentiality_e:
"weak_confidentiality_new_e (hyperc' (TEEC_FINALIZECONTEXT tctext))"
using TEEC_FinalizeContextR_weak_confidentiality weak_confidentiality_new_e_def get_exec_primeR_def
by (smt (verit) Pair_inject)
subsubsection "TEEC_OpenSession1R"
lemma TEEC_OpenSession1R_integrity:
assumes p1: "a = hyperc' (TEEC_OPENSESSION1 tct tst uuid cm cd opt mem_t)"
shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_eventR s a)) ∖↝ d)
∧ (s, s') ∈ exec_eventR a ⟶ (s ∼. d .∼Δ s')"
proof -
{
fix s' s d
assume a1: "reachable0 s"
assume a2: "((the (domain_of_eventR s a)) ∖↝ d)"
assume a3: "(s,s') ∈ exec_eventR a"
have b1:"s'=fst (TEEC_OpenSession1R sysconf s tct tst uuid cm cd opt mem_t)"
using exec_eventR_def a3 p1 by simp
have b2:"(s ∼. d .∼Δ s')" using TEEC_OpenSession1R_notchnew b1 by blast
} then show ?thesis by blast
qed
lemma TEEC_OpenSession1R_integrity_e:
"integrity_new_e (hyperc' (TEEC_OPENSESSION1 tct tst uuid cm cd opt mem_t))"
using TEEC_OpenSession1R_integrity integrity_new_e_def
by metis
lemma TEEC_OpenSession1R_weak_confidentiality:
assumes p1: "a = hyperc' (TEEC_OPENSESSION1 tct tst uuid cm cd opt mem_t)"
shows "∀ d s t.
reachable0 s ∧
reachable0 t ∧
(s ∼. d .∼ t) ∧
((domain_of_eventR s a) = (domain_of_eventR t a)) ∧
(get_exec_primeR s=get_exec_primeR t) ∧
((the (domain_of_eventR s a)) ↝ d) ∧
(s ∼. (the (domain_of_eventR s a)) .∼ t) ⟶
(∀ s' t'. (s, s') ∈ exec_eventR a ∧ (t, t') ∈ exec_eventR a ⟶ (s' ∼. d .∼Δ t'))"
proof -
{
fix s t d s' t'
assume a1:"reachable0 s"
assume a2:"reachable0 t"
assume a3:"s∼.d.∼t"
assume a31:"exec_prime s=exec_prime t"
assume a4:"(domain_of_eventR s a) = (domain_of_eventR t a)"
assume a5:"(the (domain_of_eventR s a)) ↝ d"
assume a6:"s ∼. (the (domain_of_eventR s a)) .∼ t"
assume a7:"(s, s') ∈ exec_eventR a"
assume a8:"(t, t') ∈ exec_eventR a"
have b1:"s'=fst (TEEC_OpenSession1R sysconf s tct tst uuid cm cd opt mem_t)"
using exec_eventR_def a7 p1 by simp
have b2:"t'=fst (TEEC_OpenSession1R sysconf t tct tst uuid cm cd opt mem_t)"
using exec_eventR_def a8 p1 by simp
have b3:"s' ∼. d .∼Δ t'" using b1 b2 TEEC_OpenSession1R_notchnew a3 vpeqR_def
by (meson vpeq_ipc_symmetric_lemma vpeq_ipc_transitive_lemma)
} then show ?thesis using get_exec_primeR_def
by (smt (verit, best) prod.inject)
qed
lemma TEEC_OpenSession1R_weak_confidentiality_e:
"weak_confidentiality_new_e (hyperc' (TEEC_OPENSESSION1 tct tst uuid cm cd opt mem_t))"
using TEEC_OpenSession1R_weak_confidentiality weak_confidentiality_new_e_def get_exec_primeR_def
by (smt (verit) Pair_inject)
subsubsection "TEEC_OpenSession2R"
lemma TEEC_OpenSession2R_integrity:
assumes p1: "a = hyperc' (TEEC_OPENSESSION2)"
shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_eventR s a)) ∖↝ d) ∧ (s, s') ∈ exec_eventR a ⟶ (s ∼. d .∼Δ s')"
proof -
{
fix s s' d
assume a1: "reachable0 s"
assume a2: "((the (domain_of_eventR s a)) ∖↝ d)"
assume a3: "(s,s') ∈ exec_eventR a"
let ?exec = "exec_prime s"
let ?p = "fst (hd (?exec))"
let ?opt = "the(param3 ?p)"
let ?uuid = "the (param1 ?p)"
let ?cli = "the (param4 ?p)"
let ?ctx1 = "the (param5 ?p)"
let ?memt0 = "(the (param10 ?p),the (param11 ?p))"
let ?s1 = "s⦇exec_prime:=tl ?exec⦈"
let ?s2 = "Driver_Read ?s1 smc_ex_init_read zx_mgr"
let ?s3 = "fst(ioctrlR sysconf ?s2 ?uuid ?opt ?cli ?ctx1 ?memt0)"
have a4:"s'=fst(TEEC_OpenSession2R sysconf s)"
using exec_eventR_def a3 p1 by simp
have "(s ∼. d .∼Δ s')"
proof(cases "current s≠TEE sysconf∨(exec_prime s) =[]∨snd (hd (exec_prime s)) ≠TEEC_OP2")
case True
then show ?thesis using TEEC_OpenSession2R_def a4 by fastforce
next
case False
then have b0:"¬ (current s ≠ TEE sysconf ∨ exec_prime s = [] ∨ snd (hd (exec_prime s)) ≠ TEEC_OP2)" by simp
show ?thesis
proof(cases "d=TEE sysconf")
case True
show ?thesis using True a2 interference1_def b0 domain_of_eventR_def by simp
next
case False
have b4:"d≠TEE sysconf" using False by simp
show ?thesis
proof(cases "d=REE sysconf")
case True
then show ?thesis using True a2 interference1_def b0 domain_of_eventR_def by auto
next
case False
then have b5:"d≠REE sysconf" by simp
have b6:"is_TA sysconf d" using b4 b5 by auto
then show ?thesis using b6 a2 interference1_def by simp
qed
qed
qed
}
thus ?thesis
using vpeq_transitive_lemma by blast
qed
lemma TEEC_OpenSession2R_integrity_e:
"integrity_new_e (hyperc' (TEEC_OPENSESSION2))"
using TEEC_OpenSession2R_integrity integrity_new_e_def
by metis
lemma TEEC_OpenSession2R_weak_confidentiality:
assumes p1: "a = hyperc' (TEEC_OPENSESSION2)"
shows "∀ d s t.
reachable0 s ∧
reachable0 t ∧
(s ∼. d .∼ t) ∧
((domain_of_eventR s a) = (domain_of_eventR t a)) ∧
(get_exec_primeR s=get_exec_primeR t)∧
((the (domain_of_eventR s a)) ↝ d) ∧
(s ∼. (the (domain_of_eventR s a)) .∼ t) ⟶
(∀ s' t'. (s, s') ∈ exec_eventR a ∧ (t, t') ∈ exec_eventR a ⟶ (s' ∼. d .∼Δ t'))"
proof -
{
fix s t d s' t'
assume a1:"reachable0 s"
assume a2:"reachable0 t"
assume a3:"s∼.d.∼t"
assume a31:"exec_prime s=exec_prime t"
assume a4:"(domain_of_eventR s a) = (domain_of_eventR t a)"
assume a5:"(the (domain_of_eventR s a)) ↝ d"
assume a6:"s ∼. (the (domain_of_eventR s a)) .∼ t"
assume a7:"(s, s') ∈ exec_eventR a"
assume a8:"(t, t') ∈ exec_eventR a"
let ?exec = "exec_prime s"
let ?p = "fst (hd (?exec))"
let ?opt = "the(param3 ?p)"
let ?uuid = "the (param1 ?p)"
let ?cli = "the (param4 ?p)"
let ?ctx1 = "the (param5 ?p)"
let ?memt0 = "(the (param10 ?p),the (param11 ?p))"
let ?s1 = "s⦇exec_prime:=tl ?exec⦈"
let ?t1 = "t⦇exec_prime:=tl ?exec⦈"
let ?s2 = "Driver_Read ?s1 smc_ex_init_read zx_mgr"
let ?t2 = "Driver_Read ?t1 smc_ex_init_read zx_mgr"
let ?s3 = "fst(ioctrlR sysconf ?s2 ?uuid ?opt ?cli ?ctx1 ?memt0)"
let ?t3 = "fst(ioctrlR sysconf ?t2 ?uuid ?opt ?cli ?ctx1 ?memt0)"
have "(s' ∼. d .∼Δ t')"
proof -
{
have b1:"s'=fst(TEEC_OpenSession2R sysconf s)"
using exec_eventR_def p1 a7 by simp
have b2:"t'=fst(TEEC_OpenSession2R sysconf t)"
using exec_eventR_def p1 a8 by simp
have b3:"current s=current t"
using domain_of_eventR_def a4 by simp
show ?thesis
proof(cases"(exec_prime s) =[]∨snd (hd (exec_prime s)) ≠TEEC_OP2∨current s≠TEE sysconf")
case True
then have c1:"(exec_prime s) =[]∨snd (hd (exec_prime s)) ≠TEEC_OP2∨current s≠TEE sysconf" by simp
have c2:"s'=s" using c1 b1 TEEC_OpenSession2R_def by auto
have c3:"t'=t" using c1 b2 TEEC_OpenSession2R_def a31 b3 by auto
then show ?thesis using a3 c2 c3 vpeq_ipc_def by simp
next
case False
then have c4:"¬((exec_prime s) =[]∨snd (hd (exec_prime s)) ≠TEEC_OP2∨current s≠TEE sysconf)" by simp
show ?thesis
proof(cases "d=TEE sysconf")
case True
have d1: "vpeq_ipc ?s1 d ?t1" using a3 by auto
have d2: "vpeq_ipc ?s2 d ?t2" using d1 Driver_Read_def by simp
have d3: "vpeq_ipc ?s3 d ?t3" using d2 ioctrlR_notchnew
by (smt (verit) vpeq_ipc_symmetric_lemma vpeq_ipc_transitive_lemma)
have d4: "?s3=s'" using c4 TEEC_OpenSession2R_def b1 by metis
have d5: "?t3=t'" using c4 TEEC_OpenSession2R_def b1 a31 b2 b3 by metis
show ?thesis using d3 d4 d5 by blast
next
case False
then have c6:"d≠TEE sysconf" by simp
then show ?thesis
proof(cases "d=REE sysconf")
case True
then show ?thesis using c6 is_TEE_def vpeq_ipc_def by presburger
next
case False
then have c7:"is_TA sysconf d" using is_TA_def c6 by blast
then have c8:"(s' ∼. d .∼Δ t') =True" by auto
then show ?thesis by auto
qed
qed
qed
}
qed
}
then show ?thesis using get_exec_primeR_def
by (smt (verit, best) Pair_inject)
qed
lemma TEEC_OpenSession2R_weak_confidentiality_e:
"weak_confidentiality_new_e (hyperc' (TEEC_OPENSESSION2))"
using TEEC_OpenSession2R_weak_confidentiality weak_confidentiality_new_e_def get_exec_primeR_def
by (smt (verit) Pair_inject)
subsubsection "TEEC_OpenSession3R"
lemma TEEC_OpenSession3R_integrity:
assumes p1: "a = hyperc' (TEEC_OPENSESSION3 sid)"
shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_eventR s a)) ∖↝ d) ∧ (s, s') ∈ exec_eventR a ⟶ (s ∼. d .∼Δ s')"
proof -
{
fix s s' d
assume a1: "reachable0 s"
assume a2: "((the (domain_of_eventR s a)) ∖↝ d)"
assume a3: "(s,s') ∈ exec_eventR a"
let ?domain = "the (domain_of_eventR s a)"
let ?exec = "exec_prime s"
let ?p = "fst (hd (?exec))"
let ?ses_id = "the (param2 ?p)"
let ?opt = "the(param3 ?p)"
let ?uuid = "the (param1 ?p)"
let ?ctx1 = "the (param5 ?p)"
let ?s0 = "s⦇exec_prime:=tl ?exec⦈"
let ?s1 = "?s0⇓(initTAProcess (⇑?s0) ?opt ?uuid ?ses_id)"
let ?s2 ="TA_OpenSessionEntryPointR sysconf ?s1 ?opt ?uuid"
let ?param="⦇param1=Some ?uuid,param2=Some ?ses_id,param3=None,param4=None,
param5=None,param6=None,param7=None,param8=None,param9=None,param10=None,param11=None,param12=Some TEEC_SUCCESS, param13=None⦈"
let ?s5= "?s2⦇current:=TEE sysconf,exec_prime:=(?param,TEEC_OP4)#(exec_prime ?s2)⦈"
have a4: "exec_eventR a = {(s,s'). s'∈{fst (TEEC_OpenSession3R sysconf s sid)}}"
using p1 exec_eventR_def
by auto
have a41: "s' = fst (TEEC_OpenSession3R sysconf s sid)" using a3 a4 by auto
have a5: "s≠s'⟶((the (domain_of_eventR s a)) ∖↝ (TEE sysconf))"
by (metis a2 ins_no_intf_tee ins_tee_intf_all non_interference1_def)
have a6: "?domain ≠d" using a2 nintf_neq by blast
have a7: "?domain = (current s)" using domain_of_eventR_def
using p1 by auto
have "(s ∼. d .∼Δ s')"
proof(cases "?exec = []∨snd (hd ?exec)≠TEEC_OP3∨sid≠?ses_id∨TEE sysconf=current s∨REE sysconf=current s∨current s≠?uuid")
case True
then have "s=s'" using TEEC_OpenSession3R_def a41
by force
then show ?thesis
using vpeq_ipc_reflexive_lemma by blast
next
case False
then have b1: "?exec ≠[]∧snd (hd ?exec) =TEEC_OP3∧sid=?ses_id∧TEE sysconf≠current s∧REE sysconf≠current s∧current s=?uuid" by auto
then show ?thesis
proof(cases "d = REE sysconf")
case True
then have b2:"(s ∼. d .∼Δ s') = True"
using tee_no_ree vpeq_ipc_def by auto
then show ?thesis by blast
next
case False
then have b4:"d≠REE sysconf" by simp
show ?thesis
proof(cases "d=TEE sysconf")
case True
then have b5:"d=TEE sysconf" by simp
have b7:"(s ∼. d .∼Δ s')"
proof -
{
have c1:"TEE_state ?s0 =TEE_state s"
by simp
have c2:"vpeq_ipc ?s0 (TEE sysconf) ?s1" using
abstract_state_def abstract_state_rev_def vpeq_ipc_def
by (smt (verit) Pair_inject State.ext_inject State.update_convs(1)
State.update_convs(2) State.update_convs(3) State.update_convs(4) State.update_convs(5)
State.update_convs(6) StateR.ext_inject StateR.surjective p1 surjective_pairing )
have c4:"vpeq_ipc ?s2 (TEE sysconf) ?s1"
using TA_OpenSessionEntryPointR_def vpeq_ipc_def some_eq_imp
abstract_state_def abstract_state_rev_def by auto
have c8:"s'=?s5" using TEEC_OpenSession3R_def
by (smt (verit) False State.fold_congs(6) State.unfold_congs(1) TEEC_OpenSession3_def a41 b1 fst_conv)
then show ?thesis using c4 c8 by simp
} qed
then show ?thesis by blast
next
case False
then have b8:"is_TA sysconf d" using b4 by auto
then have b9:"(s ∼. d .∼Δ s') = True" by simp
then show ?thesis by blast
qed
qed
qed
}
then show ?thesis by blast
qed
lemma TEEC_OpenSession3R_integrity_e:
"integrity_new_e (hyperc' (TEEC_OPENSESSION3 sid))"
using TEEC_OpenSession3R_integrity integrity_new_e_def
by metis
lemma TEEC_OpenSession3R_weak_confidentiality:
assumes p1: "a = hyperc' (TEEC_OPENSESSION3 sid)"
shows "∀ d s t.
reachable0 s ∧
reachable0 t ∧
(s ∼. d .∼ t) ∧
((domain_of_eventR s a) = (domain_of_eventR t a)) ∧
(get_exec_primeR s=get_exec_primeR t)∧
((the (domain_of_eventR s a)) ↝ d) ∧
(s ∼. (the (domain_of_eventR s a)) .∼ t) ⟶
(∀ s' t'. (s, s') ∈ exec_eventR a ∧ (t, t') ∈ exec_eventR a ⟶ (s' ∼. d .∼Δ t'))"
proof -
{
fix s t d s' t'
assume a1:"reachable0 s"
assume a2:"reachable0 t"
assume a3:"s∼.d.∼t"
assume a31:"exec_prime s=exec_prime t"
assume a4:"(domain_of_eventR s a) = (domain_of_eventR t a)"
assume a5:"(the (domain_of_eventR s a)) ↝ d"
assume a6:"s ∼. (the (domain_of_eventR s a)) .∼ t"
assume a7:"(s, s') ∈ exec_eventR a"
assume a8:"(t, t') ∈ exec_eventR a"
let ?domain = "the (domain_of_eventR s a)"
let ?exec = "exec_prime s"
let ?p = "fst (hd (?exec))"
let ?ses_id = "the (param2 ?p)"
let ?opt = "the(param3 ?p)"
let ?uuid = "the (param1 ?p)"
let ?ctx1 = "the (param5 ?p)"
let ?s0 = "s⦇exec_prime:=tl ?exec⦈"
let ?s1 = "?s0⇓(initTAProcess (⇑?s0) ?opt ?uuid ?ses_id)"
let ?s2 ="TA_OpenSessionEntryPointR sysconf ?s1 ?opt ?uuid"
let ?exec_t = "exec_prime s"
let ?t0 = "t⦇exec_prime:=tl ?exec_t⦈"
let ?t1 = "?t0⇓(initTAProcess (⇑?t0) ?opt ?uuid ?ses_id)"
let ?t2 ="TA_OpenSessionEntryPointR sysconf ?t1 ?opt ?uuid"
let ?param="⦇param1=Some ?uuid,param2=Some ?ses_id,param3=None,param4=None,
param5=None,param6=None,param7=None,param8=None,param9=None,param10=None,param11=None,param12=Some TEEC_SUCCESS, param13=None⦈"
let ?s5= "?s2⦇current:=TEE sysconf,exec_prime:=(?param,TEEC_OP4)#(exec_prime ?s2)⦈"
let ?t5= "?t2⦇current:=TEE sysconf,exec_prime:=(?param,TEEC_OP4)#(exec_prime ?t2)⦈"
have "(s' ∼. d .∼Δ t')"
proof -
{
have b1:"s'=fst(TEEC_OpenSession3R sysconf s sid)"
using exec_eventR_def p1 a7 by simp
have b2:"t'=fst(TEEC_OpenSession3R sysconf t sid)"
using exec_eventR_def p1 a8 by simp
have b3:"current s=current t"
using domain_of_eventR_def a4 by simp
show ?thesis
proof(cases "?exec = []∨snd (hd ?exec)≠TEEC_OP3∨sid≠?ses_id∨TEE sysconf=current s∨REE sysconf=current s∨?uuid≠current s")
case True
then have c1:"?exec = []∨snd (hd ?exec)≠TEEC_OP3∨sid≠?ses_id∨TEE sysconf=current s∨REE sysconf=current s∨?uuid≠current s" by simp
have c2:"s'=s" using c1 b1 TEEC_OpenSession3R_def by auto
have c3:"t'=t" using c1 b2 TEEC_OpenSession3R_def a31 b3 by auto
then show ?thesis using a3 c2 c3 vpeq_ipc_def by simp
next
case False
then have c4:"¬(?exec = []∨snd (hd ?exec)≠TEEC_OP3∨sid≠?ses_id∨TEE sysconf=current s∨REE sysconf=current s∨?uuid≠current s)" by simp
then have c5:"is_TA sysconf (current s)" using is_TA_def by blast
show ?thesis
proof(cases "d=TEE sysconf")
case True
then show ?thesis using a5 c5 using domain_of_eventR_def by force
next
case False
then have c6:"d≠TEE sysconf" by simp
then show ?thesis
proof(cases "d=REE sysconf")
case True
then show ?thesis using a5 c5 using domain_of_eventR_def by force
next
case False
then have c7:"is_TA sysconf d" using is_TA_def c6 by blast
then have c8:"(s' ∼. d .∼Δ t') =True" by auto
then show ?thesis by auto
qed
qed
qed
}qed
}
then show ?thesis using get_exec_primeR_def
by (smt (verit, best) Pair_inject)
qed
lemma TEEC_OpenSession3R_weak_confidentiality_e:
"weak_confidentiality_new_e (hyperc' (TEEC_OPENSESSION3 sid))"
using TEEC_OpenSession3R_weak_confidentiality weak_confidentiality_new_e_def get_exec_primeR_def
by (smt (verit) Pair_inject)
subsubsection "TEEC_OpenSession4R"
lemma TEEC_OpenSession4R_integrity:
assumes p1: "a = hyperc' (TEEC_OPENSESSION4)"
shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_eventR s a)) ∖↝ d) ∧ (s, s') ∈ exec_eventR a ⟶ (s ∼. d .∼Δ s')"
proof -
{
fix s s' d
assume a1: "reachable0 s"
assume a2: "((the (domain_of_eventR s a)) ∖↝ d)"
assume a3: "(s,s') ∈ exec_eventR a"
let ?exec = "exec_prime s"
let ?p = "fst (hd (?exec))"
have a4:"s'=fst(TEEC_OpenSession4R sysconf s)"
using exec_eventR_def a3 p1 by simp
have "(s ∼. d .∼Δ s')"
proof(cases "current s≠TEE sysconf∨(exec_prime s) =[]∨snd (hd (exec_prime s)) ≠TEEC_OP4")
case True
then show ?thesis using TEEC_OpenSession4R_def a4 by fastforce
next
case False
then have b0:"¬ (current s ≠ TEE sysconf ∨ exec_prime s = [] ∨ snd (hd (exec_prime s)) ≠ TEEC_OP4)" by simp
show ?thesis
proof(cases "d=TEE sysconf")
case True
show ?thesis using True a2 interference1_def b0 domain_of_eventR_def by simp
next
case False
have b4:"d≠TEE sysconf" using False by simp
show ?thesis
proof(cases "d=REE sysconf")
case True
then show ?thesis using True a2 interference1_def b0 domain_of_eventR_def by auto
next
case False
then have b5:"d≠REE sysconf" by simp
have b6:"is_TA sysconf d" using b4 b5 by auto
then show ?thesis using b6 a2 interference1_def by simp
qed
qed
qed
}
thus ?thesis
using vpeq_transitive_lemma by blast
qed
lemma TEEC_OpenSession4R_integrity_e:
"integrity_new_e (hyperc' (TEEC_OPENSESSION4))"
using TEEC_OpenSession4R_integrity integrity_new_e_def
by metis
lemma TEEC_OpenSession4R_weak_confidentiality:
assumes p1: "a = hyperc' (TEEC_OPENSESSION4)"
shows "∀ d s t.
reachable0 s ∧
reachable0 t ∧
(s ∼. d .∼ t) ∧
((domain_of_eventR s a) = (domain_of_eventR t a)) ∧
(get_exec_primeR s=get_exec_primeR t)∧
((the (domain_of_eventR s a)) ↝ d) ∧
(s ∼. (the (domain_of_eventR s a)) .∼ t) ⟶
(∀ s' t'. (s, s') ∈ exec_eventR a ∧ (t, t') ∈ exec_eventR a ⟶ (s' ∼. d .∼Δ t'))"
proof -
{
fix s t d s' t'
assume a1:"reachable0 s"
assume a2:"reachable0 t"
assume a3:"s∼.d.∼t"
assume a31:"exec_prime s=exec_prime t"
assume a4:"(domain_of_eventR s a) = (domain_of_eventR t a)"
assume a5:"(the (domain_of_eventR s a)) ↝ d"
assume a6:"s ∼. (the (domain_of_eventR s a)) .∼ t"
assume a7:"(s, s') ∈ exec_eventR a"
assume a8:"(t, t') ∈ exec_eventR a"
let ?exec="exec_prime s"
let ?p = "fst (hd ?exec)"
let ?tid1 =" the (param1 ?p)"
let ?ses_id =" the (param2 ?p)"
let ?res3= "the (param12 ?p)"
let ?param="⦇param1=Some ?ses_id,param2=Some ?tid1,param3=None,param4=Some ⦇login=DTC_IDENTITY,id=Some 0⦈,
param5=None,param6=None,param7=None,param8=None,param9=None,
param10=None,param11=None,param12=None,param13=None⦈"
let ?smc_ex = "⦇a0=0,a1=0,a2=0,a3= ?ses_id,a4=0,a5=0,a6=0,a7=0,u2k=0,k2u=0⦈"
let ?s1="s⦇exec_prime:=tl ?exec⦈"
let ?t1="t⦇exec_prime:=tl ?exec⦈"
let ?s2="?s1⇓(MgrPostOperation (⇑?s1) ?tid1)"
let ?t2="?t1⇓(MgrPostOperation (⇑?t1) ?tid1)"
let ?s3="?s2⦇current:=TEE sysconf,exec_prime:=(?param,TEEC_CS2)#(exec_prime ?s2)⦈"
let ?t3="?t2⦇current:=TEE sysconf,exec_prime:=(?param,TEEC_CS2)#(exec_prime ?t2)⦈"
let ?s4="fst(Driver_Write_smc ?s3 zx_mgr ZX_ERR_INTERNALr smc_ex_init)"
let ?s42="fst(Driver_Write_smc ?s2 zx_mgr ZX_OKr ?smc_ex)"
let ?t4="fst(Driver_Write_smc ?t3 zx_mgr ZX_ERR_INTERNALr smc_ex_init)"
let ?t42="fst(Driver_Write_smc ?t2 zx_mgr ZX_OKr ?smc_ex)"
have "(s' ∼. d .∼Δ t')"
proof -
{
have b1:"s'=fst(TEEC_OpenSession4R sysconf s)"
using exec_eventR_def p1 a7 by simp
have b2:"t'=fst(TEEC_OpenSession4R sysconf t)"
using exec_eventR_def p1 a8 by simp
have b3:"current s=current t"
using domain_of_eventR_def a4 by simp
show ?thesis
proof(cases"(exec_prime s) =[]∨snd (hd (exec_prime s)) ≠TEEC_OP4∨current s≠TEE sysconf")
case True
then have c1:"(exec_prime s) =[]∨snd (hd (exec_prime s)) ≠TEEC_OP4∨current s≠TEE sysconf" by simp
have c2:"s'=s" using c1 b1 TEEC_OpenSession4R_def by auto
have c3:"t'=t" using c1 b2 TEEC_OpenSession4R_def a31 b3 by auto
then show ?thesis using a3 c2 c3 vpeq_ipc_def by simp
next
case False
then have c4:"¬((exec_prime s) =[]∨snd (hd (exec_prime s)) ≠TEEC_OP4∨current s≠TEE sysconf)" by simp
show ?thesis
proof -
{
have d1: "vpeq_ipc ?s1 d ?t1" using a3 by auto
have d2: "vpeq_ipc ?s2 d ?t2" using d1 MgrPostOperation_def by auto
have d3: "vpeq_ipc ?s3 d ?t3" using d2 by auto
have d4: "vpeq_ipc ?s4 d ?t4" using d3 Driver_Write_smc_def by auto
have d5: "vpeq_ipc ?s42 d ?t42" using d2 Driver_Write_smc_def by auto
show ?thesis
proof(cases"?res3=TEEC_SUCCESS")
case True
then have e1:"?res3=TEEC_SUCCESS" by simp
show ?thesis
proof -
{
have e2:"s'=?s42"
using c4 b1 e1 TEEC_OpenSession4R_def
by (smt (verit, best) State.fold_congs(6) fst_conv)
have e3:"t'=?t42"
using c4 b2 e1 b3 a31 TEEC_OpenSession4R_def
by (smt (verit, best) State.fold_congs(6) fst_conv)
show ?thesis using e2 e3 d5 by argo
}qed
next
case False
then have e4:"?res3≠TEEC_SUCCESS" by simp
show ?thesis
proof -
{
have e2:"s'=?s4"
using c4 b1 e4 TEEC_OpenSession4R_def State.fold_congs(6) fst_conv
by (smt (verit) State.unfold_congs(1))
have e3:"t'=?t4"
using c4 b2 e4 b3 a31 TEEC_OpenSession4R_def
by (smt (verit, best) State.unfold_congs(1) State.fold_congs(6) fst_conv)
show ?thesis using e2 e3 d4 by argo
}qed
qed
}
qed
qed
}
qed
}
then show ?thesis using get_exec_primeR_def
by (smt (verit, best) Pair_inject)
qed
lemma TEEC_OpenSession4R_weak_confidentiality_e:
"weak_confidentiality_new_e (hyperc' (TEEC_OPENSESSION4))"
using TEEC_OpenSession4R_weak_confidentiality weak_confidentiality_new_e_def get_exec_primeR_def
by (smt (verit) Pair_inject)
subsection "TEE side"
subsubsection "TEE_OpenTASession1R"
lemma TEE_OpenTASession1R_integrity:
assumes p1: "a = hyperc' (TEE_OPENTASESSION1)"
shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_eventR s a)) ∖↝ d)
∧ (s, s') ∈ exec_eventR a ⟶ (s ∼. d .∼Δ s')"
proof -
{
fix s' s d
assume a1: "reachable0 s"
assume a2: "((the (domain_of_eventR s a)) ∖↝ d)"
assume a3: "(s,s') ∈ exec_eventR a"
have b1:"s'=fst (TEE_OpenTASession1R sysconf s)"
using exec_eventR_def a3 p1 by simp
have b2:"(s ∼. d .∼Δ s')" using TEE_OpenTASession1R_notchnew b1 by blast
} then show ?thesis by blast
qed
lemma TEE_OpenTASession1R_integrity_e:
"integrity_new_e (hyperc' (TEE_OPENTASESSION1))"
using TEE_OpenTASession1R_integrity integrity_new_e_def
by metis
lemma TEE_OpenTASession1R_weak_confidentiality:
assumes p1: "a = hyperc' (TEE_OPENTASESSION1)"
shows "∀ d s t.
reachable0 s ∧
reachable0 t ∧
(s ∼. d .∼ t) ∧
((domain_of_eventR s a) = (domain_of_eventR t a)) ∧
(get_exec_primeR s=get_exec_primeR t) ∧
((the (domain_of_eventR s a)) ↝ d) ∧
(s ∼. (the (domain_of_eventR s a)) .∼ t) ⟶
(∀ s' t'. (s, s') ∈ exec_eventR a ∧ (t, t') ∈ exec_eventR a ⟶ (s' ∼. d .∼Δ t'))"
proof -
{
fix s t d s' t'
assume a1:"reachable0 s"
assume a2:"reachable0 t"
assume a3:"s∼.d.∼t"
assume a31:"exec_prime s=exec_prime t"
assume a4:"(domain_of_eventR s a) = (domain_of_eventR t a)"
assume a5:"(the (domain_of_eventR s a)) ↝ d"
assume a6:"s ∼. (the (domain_of_eventR s a)) .∼ t"
assume a7:"(s, s') ∈ exec_eventR a"
assume a8:"(t, t') ∈ exec_eventR a"
have b1:"s'=fst (TEE_OpenTASession1R sysconf s)"
using exec_eventR_def a7 p1 by simp
have b2:"t'=fst (TEE_OpenTASession1R sysconf t)"
using exec_eventR_def a8 p1 by simp
have b3:"s' ∼. d .∼Δ t'" using b1 b2 TEE_OpenTASession1R_notchnew a3 vpeqR_def
by (meson vpeq_ipc_symmetric_lemma vpeq_ipc_transitive_lemma)
} then show ?thesis using get_exec_primeR_def
by (smt (verit, best) prod.inject)
qed
lemma TEE_OpenTASession1R_weak_confidentiality_e:
"weak_confidentiality_new_e (hyperc' (TEE_OPENTASESSION1))"
using TEE_OpenTASession1R_weak_confidentiality weak_confidentiality_new_e_def get_exec_primeR_def
by (smt (verit) Pair_inject)
subsubsection "TEE_OpenTASession2R"
lemma TEE_OpenTASession2R_integrity:
assumes p1: "a = hyperc' (TEE_OPENTASESSION2)"
shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_eventR s a)) ∖↝ d)
∧ (s, s') ∈ exec_eventR a ⟶ (s ∼. d .∼Δ s')"
proof -
{
fix s' s d
assume a1: "reachable0 s"
assume a2: "((the (domain_of_eventR s a)) ∖↝ d)"
assume a3: "(s,s') ∈ exec_eventR a"
have b1:"s'=fst (TEE_OpenTASession2R sysconf s)"
using exec_eventR_def a3 p1 by simp
have b2:"(s ∼. d .∼Δ s')" using TEE_OpenTASession2R_notchnew b1 by blast
} then show ?thesis by blast
qed
lemma TEE_OpenTASession2R_integrity_e:
"integrity_new_e (hyperc' (TEE_OPENTASESSION2))"
using TEE_OpenTASession2R_integrity integrity_new_e_def
by metis
lemma TEE_OpenTASession2R_weak_confidentiality:
assumes p1: "a = hyperc' (TEE_OPENTASESSION2)"
shows "∀ d s t.
reachable0 s ∧
reachable0 t ∧
(s ∼. d .∼ t) ∧
((domain_of_eventR s a) = (domain_of_eventR t a)) ∧
(get_exec_primeR s=get_exec_primeR t) ∧
((the (domain_of_eventR s a)) ↝ d) ∧
(s ∼. (the (domain_of_eventR s a)) .∼ t) ⟶
(∀ s' t'. (s, s') ∈ exec_eventR a ∧ (t, t') ∈ exec_eventR a ⟶ (s' ∼. d .∼Δ t'))"
proof -
{
fix s t d s' t'
assume a1:"reachable0 s"
assume a2:"reachable0 t"
assume a3:"s∼.d.∼t"
assume a31:"exec_prime s=exec_prime t"
assume a4:"(domain_of_eventR s a) = (domain_of_eventR t a)"
assume a5:"(the (domain_of_eventR s a)) ↝ d"
assume a6:"s ∼. (the (domain_of_eventR s a)) .∼ t"
assume a7:"(s, s') ∈ exec_eventR a"
assume a8:"(t, t') ∈ exec_eventR a"
have b1:"s'=fst (TEE_OpenTASession2R sysconf s)"
using exec_eventR_def a7 p1 by simp
have b2:"t'=fst (TEE_OpenTASession2R sysconf t)"
using exec_eventR_def a8 p1 by simp
have b3:"s' ∼. d .∼Δ t'" using b1 b2 TEE_OpenTASession2R_notchnew a3 vpeqR_def
by (meson vpeq_ipc_symmetric_lemma vpeq_ipc_transitive_lemma)
} then show ?thesis using get_exec_primeR_def
by (smt (verit, best) prod.inject)
qed
lemma TEE_OpenTASession2R_weak_confidentiality_e:
"weak_confidentiality_new_e (hyperc' (TEE_OPENTASESSION2))"
using TEE_OpenTASession2R_weak_confidentiality weak_confidentiality_new_e_def get_exec_primeR_def
by (smt (verit) Pair_inject)
subsubsection "TEEC_OpenSession3R"
lemma TEE_OpenTASession3R_integrity:
assumes p1: "a = hyperc' (TEE_OPENTASESSION3 sid)"
shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_eventR s a)) ∖↝ d) ∧ (s, s') ∈ exec_eventR a ⟶ (s ∼. d .∼Δ s')"
proof -
{
fix s s' d
assume a1: "reachable0 s"
assume a2: "((the (domain_of_eventR s a)) ∖↝ d)"
assume a3: "(s,s') ∈ exec_eventR a"
let ?domain = "the (domain_of_eventR s a)"
let ?exec = "exec_prime s"
let ?p = "fst (hd (?exec))"
let ?ses_id = "the (param2 ?p)"
let ?opt = "the(param3 ?p)"
let ?uuid = "the (param1 ?p)"
let ?ctx1 = "the (param5 ?p)"
let ?s0 = "s⦇exec_prime:=tl ?exec⦈"
let ?s1 = "?s0⇓(initTAProcess (⇑?s0) ?opt ?uuid ?ses_id)"
let ?s2 ="TA_OpenSessionEntryPointR sysconf ?s1 ?opt ?uuid"
let ?param="⦇param1=Some ?uuid,param2=Some ?ses_id,param3=None,param4=None,
param5=None,param6=None,param7=None,param8=None,param9=None,param10=None,param11=None,param12=None, param13=Some TEE_SUCCESS⦈"
let ?s5= "?s2⦇current:=TEE sysconf,exec_prime:=(?param,TEE_OP4)#(exec_prime ?s2)⦈"
have a4: "exec_eventR a = {(s,s'). s'∈{fst (TEE_OpenTASession3R sysconf s sid)}}"
using p1 exec_eventR_def
by auto
have a41: "s' = fst (TEE_OpenTASession3R sysconf s sid)" using a3 a4 by auto
have a5: "s≠s'⟶((the (domain_of_eventR s a)) ∖↝ (TEE sysconf))"
by (metis a2 ins_no_intf_tee ins_tee_intf_all non_interference1_def)
have a6: "?domain ≠d" using a2 nintf_neq by blast
have a7: "?domain = (current s)" using domain_of_eventR_def
using p1 by auto
have "(s ∼. d .∼Δ s')"
proof(cases "?exec = []∨snd (hd ?exec)≠TEE_OP3∨sid≠?ses_id∨TEE sysconf=current s∨REE sysconf=current s∨current s≠?uuid")
case True
then have "s=s'" using TEE_OpenTASession3R_def a41
by force
then show ?thesis
using vpeq_ipc_reflexive_lemma by blast
next
case False
then have b1: "?exec ≠[]∧snd (hd ?exec) =TEE_OP3∧sid=?ses_id∧TEE sysconf≠current s∧REE sysconf≠current s∧current s=?uuid" by auto
then show ?thesis
proof(cases "d = REE sysconf")
case True
then have b2:"(s ∼. d .∼Δ s') = True"
using tee_no_ree vpeq_ipc_def by auto
then show ?thesis by blast
next
case False
then have b4:"d≠REE sysconf" by simp
show ?thesis
proof(cases "d=TEE sysconf")
case True
then have b5:"d=TEE sysconf" by simp
have b7:"(s ∼. d .∼Δ s')"
proof -
{
have c1:"TEE_state ?s0 =TEE_state s"
by simp
have c2:"vpeq_ipc ?s0 (TEE sysconf) ?s1" using
abstract_state_def abstract_state_rev_def vpeq_ipc_def
by (smt (verit) Pair_inject State.ext_inject State.update_convs(1)
State.update_convs(2) State.update_convs(3) State.update_convs(4) State.update_convs(5)
State.update_convs(6) StateR.ext_inject StateR.surjective p1 surjective_pairing )
have c4:"vpeq_ipc ?s2 (TEE sysconf) ?s1"
using TA_OpenSessionEntryPointR_def vpeq_ipc_def some_eq_imp
abstract_state_def abstract_state_rev_def by auto
have c8:"s'=?s5" using TEE_OpenTASession3R_def
by (smt (verit) False State.fold_congs(6) State.unfold_congs(1) TEE_OpenTASession3_def a41 b1 fst_conv)
then show ?thesis using c4 c8 by simp
} qed
then show ?thesis by blast
next
case False
then have b8:"is_TA sysconf d" using b4 by auto
then have b9:"(s ∼. d .∼Δ s') = True" by simp
then show ?thesis by blast
qed
qed
qed
}
then show ?thesis by blast
qed
lemma TEE_OpenTASession3R_integrity_e:
"integrity_new_e (hyperc' (TEE_OPENTASESSION3 sid))"
using TEE_OpenTASession3R_integrity integrity_new_e_def
by metis
lemma TEE_OpenTASession3R_weak_confidentiality:
assumes p1: "a = hyperc' (TEE_OPENTASESSION3 sid)"
shows "∀ d s t.
reachable0 s ∧
reachable0 t ∧
(s ∼. d .∼ t) ∧
((domain_of_eventR s a) = (domain_of_eventR t a)) ∧
(get_exec_primeR s=get_exec_primeR t)∧
((the (domain_of_eventR s a)) ↝ d) ∧
(s ∼. (the (domain_of_eventR s a)) .∼ t) ⟶
(∀ s' t'. (s, s') ∈ exec_eventR a ∧ (t, t') ∈ exec_eventR a ⟶ (s' ∼. d .∼Δ t'))"
proof -
{
fix s t d s' t'
assume a1:"reachable0 s"
assume a2:"reachable0 t"
assume a3:"s∼.d.∼t"
assume a31:"exec_prime s=exec_prime t"
assume a4:"(domain_of_eventR s a) = (domain_of_eventR t a)"
assume a5:"(the (domain_of_eventR s a)) ↝ d"
assume a6:"s ∼. (the (domain_of_eventR s a)) .∼ t"
assume a7:"(s, s') ∈ exec_eventR a"
assume a8:"(t, t') ∈ exec_eventR a"
let ?domain = "the (domain_of_eventR s a)"
let ?exec = "exec_prime s"
let ?p = "fst (hd (?exec))"
let ?ses_id = "the (param2 ?p)"
let ?opt = "the(param3 ?p)"
let ?uuid = "the (param1 ?p)"
let ?ctx1 = "the (param5 ?p)"
let ?s0 = "s⦇exec_prime:=tl ?exec⦈"
let ?s1 = "?s0⇓(initTAProcess (⇑?s0) ?opt ?uuid ?ses_id)"
let ?s2 ="TA_OpenSessionEntryPointR sysconf ?s1 ?opt ?uuid"
let ?exec_t = "exec_prime s"
let ?t0 = "t⦇exec_prime:=tl ?exec_t⦈"
let ?t1 = "?t0⇓(initTAProcess (⇑?t0) ?opt ?uuid ?ses_id)"
let ?t2 ="TA_OpenSessionEntryPointR sysconf ?t1 ?opt ?uuid"
let ?param="⦇param1=Some ?uuid,param2=Some ?ses_id,param3=None,param4=None,
param5=None,param6=None,param7=None,param8=None,param9=None,param10=None,param11=None,param12=None, param13=Some TEE_SUCCESS⦈"
let ?s5= "?s2⦇current:=TEE sysconf,exec_prime:=(?param,TEE_OP4)#(exec_prime ?s2)⦈"
let ?t5= "?t2⦇current:=TEE sysconf,exec_prime:=(?param,TEE_OP4)#(exec_prime ?t2)⦈"
have "(s' ∼. d .∼Δ t')"
proof -
{
have b1:"s'=fst(TEE_OpenTASession3R sysconf s sid)"
using exec_eventR_def p1 a7 by simp
have b2:"t'=fst(TEE_OpenTASession3R sysconf t sid)"
using exec_eventR_def p1 a8 by simp
have b3:"current s=current t"
using domain_of_eventR_def a4 by simp
show ?thesis
proof(cases "?exec = []∨snd (hd ?exec)≠TEE_OP3∨sid≠?ses_id∨TEE sysconf=current s∨REE sysconf=current s∨?uuid≠current s")
case True
then have c1:"?exec = []∨snd (hd ?exec)≠TEE_OP3∨sid≠?ses_id∨TEE sysconf=current s∨REE sysconf=current s∨?uuid≠current s" by simp
have c2:"s'=s" using c1 b1 TEE_OpenTASession3R_def by auto
have c3:"t'=t" using c1 b2 TEE_OpenTASession3R_def a31 b3 by auto
then show ?thesis using a3 c2 c3 vpeq_ipc_def by simp
next
case False
then have c4:"¬(?exec = []∨snd (hd ?exec)≠TEE_OP3∨sid≠?ses_id∨TEE sysconf=current s∨REE sysconf=current s∨?uuid≠current s)" by simp
then have c5:"is_TA sysconf (current s)" using is_TA_def by blast
show ?thesis
proof(cases "d=TEE sysconf")
case True
then show ?thesis using a5 c5 using domain_of_eventR_def by force
next
case False
then have c6:"d≠TEE sysconf" by simp
then show ?thesis
proof(cases "d=REE sysconf")
case True
then show ?thesis using a5 c5 using domain_of_eventR_def by force
next
case False
then have c7:"is_TA sysconf d" using is_TA_def c6 by blast
then have c8:"(s' ∼. d .∼Δ t') =True" by auto
then show ?thesis by auto
qed
qed
qed
}qed
}
then show ?thesis using get_exec_primeR_def
by (smt (verit, best) Pair_inject)
qed
lemma TEE_OpenTASession3R_weak_confidentiality_e:
"weak_confidentiality_new_e (hyperc' (TEE_OPENTASESSION3 sid))"
using TEE_OpenTASession3R_weak_confidentiality weak_confidentiality_new_e_def get_exec_primeR_def
by (smt (verit) Pair_inject)
subsubsection "TEE_OpenTASession4R"
lemma TEE_OpenTASession4R_integrity:
assumes p1: "a = hyperc' (TEE_OPENTASESSION4)"
shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_eventR s a)) ∖↝ d)
∧ (s, s') ∈ exec_eventR a ⟶ (s ∼. d .∼Δ s')"
proof -
{
fix s' s d
assume a1: "reachable0 s"
assume a2: "((the (domain_of_eventR s a)) ∖↝ d)"
assume a3: "(s,s') ∈ exec_eventR a"
have b1:"s'=fst (TEE_OpenTASession4R sysconf s)"
using exec_eventR_def a3 p1 by simp
have b2:"(s ∼. d .∼Δ s')" using TEE_OpenTASession4R_notchnew b1 by blast
} then show ?thesis by blast
qed
lemma TEE_OpenTASession4R_integrity_e:
"integrity_new_e (hyperc' (TEE_OPENTASESSION4))"
using TEE_OpenTASession4R_integrity integrity_new_e_def
by metis
lemma TEE_OpenTASession4R_weak_confidentiality:
assumes p1: "a = hyperc' (TEE_OPENTASESSION4)"
shows "∀ d s t.
reachable0 s ∧
reachable0 t ∧
(s ∼. d .∼ t) ∧
((domain_of_eventR s a) = (domain_of_eventR t a)) ∧
(get_exec_primeR s=get_exec_primeR t) ∧
((the (domain_of_eventR s a)) ↝ d) ∧
(s ∼. (the (domain_of_eventR s a)) .∼ t) ⟶
(∀ s' t'. (s, s') ∈ exec_eventR a ∧ (t, t') ∈ exec_eventR a ⟶ (s' ∼. d .∼Δ t'))"
proof -
{
fix s t d s' t'
assume a1:"reachable0 s"
assume a2:"reachable0 t"
assume a3:"s∼.d.∼t"
assume a31:"exec_prime s=exec_prime t"
assume a4:"(domain_of_eventR s a) = (domain_of_eventR t a)"
assume a5:"(the (domain_of_eventR s a)) ↝ d"
assume a6:"s ∼. (the (domain_of_eventR s a)) .∼ t"
assume a7:"(s, s') ∈ exec_eventR a"
assume a8:"(t, t') ∈ exec_eventR a"
have b1:"s'=fst (TEE_OpenTASession4R sysconf s)"
using exec_eventR_def a7 p1 by simp
have b2:"t'=fst (TEE_OpenTASession4R sysconf t)"
using exec_eventR_def a8 p1 by simp
have b3:"s' ∼. d .∼Δ t'" using b1 b2 TEE_OpenTASession4R_notchnew a3 vpeqR_def
by (meson vpeq_ipc_symmetric_lemma vpeq_ipc_transitive_lemma)
} then show ?thesis using get_exec_primeR_def
by (smt (verit, best) prod.inject)
qed
lemma TEE_OpenTASession4R_weak_confidentiality_e:
"weak_confidentiality_new_e (hyperc' (TEE_OPENTASESSION4))"
using TEE_OpenTASession4R_weak_confidentiality weak_confidentiality_new_e_def get_exec_primeR_def
by (smt (verit) Pair_inject)
end